(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v7 () Bool)
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(assert (= (or v2 (= (_ bv0 61) (_ bv0 61) (_ bv0 61) (_ bv0 61) (_ bv0 61)) v7 v0 v1 v6) v3 v5 (not v3) v4 (= (_ bv0 61) (_ bv0 61) (_ bv0 61) (_ bv0 61) (_ bv0 61)) v3))
(check-sat)
